@manuscript{Abadi:93,
title={{Types for the Scott Numerals}},
author={M. Abadi and L. Cardelli and G. Plotkin},
note="Unpublished, available from Abadi's web page",
year=1993,
pages={1--2}}                  

@book{Church:1985,
 author = {Church, Alonzo},
 title = {The Calculi of Lambda Conversion. (AM-6) (Annals of Mathematics Studies)},
 year = {1985},
 isbn = {0691083940},
 publisher = {Princeton University Press},
 address = {Princeton, NJ, USA},
} 
@book{CHS:72,
  author = {H. B. Curry and J. R. Hindley and J. P. Seldin},
  title = {Combinatory Logic, Volume II},
  publisher = {North-Holland},
  year = {1972},
  pages = {xiv+520}
}

@article{Barendregt:97,
  author    = {Henk Barendregt},
  title     = {The impact of the lambda calculus in logic and computer
               science},
  journal   = {Bulletin of Symbolic Logic},
  volume    = {3},
  number    = {2},
  year      = {1997},
  pages     = {181-215},
  ee        = {http://www.math.ucla.edu/$\sim$asl/bsl/0302/0302-003.ps},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@dissertation{Girard:72,
author="Jean-Yves Girard",
title="Interpr\'etation fonctionnelle et \'elimination des coupures de l'arithm\'etique d'ordre sup\'erieur",
institution="Universit\'e Paris VII",
year="1972"}

@book{Girard:1989,
 author = {Girard, Jean-Yves and Taylor, Paul and Lafont, Yves},
 title = {Proofs and types},
 year = {1989},
 isbn = {0-521-37181-3},
 publisher = {Cambridge University Press},
 address = {New York, NY, USA},
} 

@inproceedings{Werner:92,
author = {B. Werner},
title = {{A Normalization Proof for an Impredicative Type System with Large Elimination over Integers}},
booktitle="International Workshop on Types for Proofs and Programs (TYPES)",
year="1992",
editor={B. Nordstr\"om and K. Petersson and G. Plotkin},
pages="341--357",
}
@article{Coquand:1988,
 author = {Coquand, Thierry and Huet, Gerard},
 title = {The calculus of constructions},
 journal = {Inf. Comput.},
 issue_date = {February/March 1988},
 volume = {76},
 number = {2-3},
 month = feb,
 year = {1988},
 issn = {0890-5401},
 pages = {95--120},
 numpages = {26},
 url = {http://dx.doi.org/10.1016/0890-5401(88)90005-3},
 doi = {10.1016/0890-5401(88)90005-3},
 acmid = {47725},
 publisher = {Academic Press, Inc.},
 address = {Duluth, MN, USA},
} 
@incollection{Paulin:1993,
  title={Inductive definitions in the system coq rules and properties},
  author={Paulin-Mohring, Christine},
  booktitle={Typed lambda calculi and applications},
  pages={328--345},
  year={1993},
  publisher={Springer}
}
@article{Jansen:2011,
  author    = {J.M. Jansen and R. Plasmeijer and P. Koopman},
  title     = {Functional Pearl: Comprehensive Encoding of Data Types and Algorithms in the lambda-Calculus},
  journal   = {Internal report, NLDA},
  year      = {2011},
}
